more from this thinker     |     more from this text

Single Idea 18120

[filed under theme 5. Theory of Logic / H. Proof Systems / 4. Natural Deduction ]

Full Idea

The Deduction Theorem is what licenses a system of 'natural deduction' in the first place.

Gist of Idea

The Deduction Theorem is what licenses a system of natural deduction

Source

David Bostock (Philosophy of Mathematics [2009], 7.2)

Book Ref

Bostock,David: 'Philosophy of Mathematics: An Introduction' [Wiley-Blackwell 2009], p.202

Related Ideas

Idea 15341 Deduction Theorem: ψ only derivable from φ iff φ→ψ are axioms [Horsten]

Idea 13524 Deduction Theorem: T∪{P}|-Q, then T|-(P→Q), which justifies Conditional Proof [Wolf,RS]

Idea 13615 'Conditonalised' inferences point to the Deduction Theorem: If Γ,φ|-ψ then Γ|-φ→ψ [Bostock]

The 14 ideas with the same theme [proofs built from introduction and elimination rules]:

13832 Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) [Gentzen, by Hacking]
13753 Natural deduction takes proof from assumptions (with its rules) as basic, and axioms play no part [Bostock]
13755 Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it [Bostock]
13754 Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E) [Bostock]
13758 In natural deduction we work from the premisses and the conclusion, hoping to meet in the middle [Bostock]
18120 The Deduction Theorem is what licenses a system of natural deduction [Bostock]
13823 In natural deduction, inferences are atomic steps involving just one logical constant [Prawitz]
10602 A 'natural deduction system' has no axioms but many rules [Smith,P]
21612 Or-elimination is 'Argument by Cases'; it shows how to derive C from 'A or B' [Williamson]
13685 Natural deduction helpfully allows reasoning with assumptions [Sider]
19298 Unlike axiom proofs, natural deduction proofs needn't focus on logical truths and theorems [Hale]
18783 Many-valued logics lack a natural deduction system [Mares]
15001 'Tonk' is supposed to follow the elimination and introduction rules, but it can't be so interpreted [Sider]
18800 Introduction rules give deduction conditions, and Elimination says what can be deduced [Rumfitt]